\begin{tabbing}
es{-}responsive(${\it es}$;$l_{1}$;${\it tg}_{1}$;$l_{2}$;${\it tg}_{2}$)
\\[0ex]$\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$\=(\=$\forall$$e$=rcv($l_{1}$,${\it tg}_{1}$).\+\+
\\[0ex]$\exists$${\it e'}$=rcv($l_{2}$,${\it tg}_{2}$).
\\[0ex]$e$ $\leq$loc sender(${\it e'}$) 
\\[0ex]\& ($\forall$$e_{2}$=rcv($l_{1}$,${\it tg}_{1}$). ($e$ $<$loc $e_{2}$) $\Rightarrow$ (sender(${\it e'}$) $<$loc $e_{2}$))
\\[0ex]\& ($\forall$${\it e''}$=rcv($l_{2}$,${\it tg}_{2}$). (sender(${\it e''}$) = sender(${\it e'}$)) $\Rightarrow$ (${\it e''}$ = ${\it e'}$)))
\-\\[0ex]\& (\=$\forall$${\it e'}$=rcv($l_{2}$,${\it tg}_{2}$).\+
\\[0ex]$\exists$$e$=rcv($l_{1}$,${\it tg}_{1}$).
\\[0ex]$e$ $\leq$loc sender(${\it e'}$) 
\\[0ex]\& ($\forall$${\it e''}$=rcv($l_{2}$,${\it tg}_{2}$). (sender(${\it e''}$) $<$loc sender(${\it e'}$)) $\Rightarrow$ (sender(${\it e''}$) $<$loc $e$)))
\-\-
\end{tabbing}